Casper CBC: General validator rotation
Prerequisite
I reuse definitions and lemmas in the original paper.
Overview
Protocol
We replace the weight parameter$ \mathcal{W}with weights, which is a set of all possible weight.
Also, we limit the consensus values ($ \mathcal{C}) so that we can extract a weight.
$ \mathrm{Weight}: \mathcal{C} \rightarrow \mathcal{W}
No modification on messages, states unlike the proposal in the previous Casper TFG paper.
Helper functions
Weight measure by a given weight
$ W(V, w) :\Leftrightarrow \sum_{v \in V} w(v)
Equivocation fault weight by a given weight
$ F_\mathcal{W}(\sigma, w) := W(E(\sigma), w)
Weight estimator
$ \mathcal{E}_\mathcal{W}(\sigma) := \{w \in \mathcal{W}| ~\exists c \in \mathcal{E}(\sigma). ~w = \mathrm{Weight}(c)\}
States where there are$ tequivocations or less by the given weight
$ \Sigma_{t, \mathcal{W}}(w) := \{\sigma \in \Sigma~| ~F_W(\sigma, w) \leq t\}
Future states where there are$ tequivocations or less by a given weight
$ \mathrm{Futures}_{t, \mathcal{W}}(\sigma, w) := \{\sigma \in \Sigma~| ~\sigma \to \sigma' \land F_W(\sigma', w) \leq t\}
Past states
$ \mathrm{Pasts}(\sigma) := \{\sigma_p \in \Sigma~| ~\sigma_p \to \sigma\}
In this post, I use$ \sigma_pto represent a "past state"
Abstract safety
The new decision making rule is:
$ \mathrm{Decided}_\mathcal{W}(p, \sigma, w) := \forall \sigma' \in \mathrm{Futures}_{t, W}(\sigma, W). ~\forall c \in \mathcal{E}(\sigma'). ~p(c)
Safety (two-party version):
$ \forall p. ~\forall w \in \mathcal{W}. ~\forall \sigma_1, \sigma_2 ~\in \Sigma_{t, W}. ~\mathrm{Decided}_p(p, \sigma_1, w)
$ \implies F(\sigma_1 \cup \sigma_2, w) \leq t
$ \implies \neg ~\mathrm{Decided}_p(\neg ~p, \sigma_2, w)
This is proved similarly to Theorem 3 (Two-party consensus safety) of the original paper.
Clique oracle
We fix the definition of$ \mathrm{Agreeing}(p, \sigma)so that it does not include equivocating validators (like $ \mathrm{Disagreeing}(p, \sigma)).
Max and past-max
$ \mathrm{Max}_\mathcal{W}(\sigma, w, p) :\Leftrightarrow W(\mathrm{Agreeing}(p, \sigma), w) > W(\mathrm{Disagreeing}(p, \sigma), w)
Max-driven property parameterized by a weight
$ \mathrm{Max\_Driven}_t(p, w) :\Leftrightarrow \forall \sigma \in \Sigma. ~\mathrm{Max}_\mathcal{W}(\sigma, w, p) \implies \forall c \in \mathcal{E}(\sigma). ~p(c)
Threshold for past-max-driven clique oracle
$ \mathrm{Threshold}_{t, \mathcal{W}}(V, \sigma, w) :\Leftrightarrow W(V, w) > W(\mathcal{V}, w)/2 + t/2 - F_W(\sigma, w)
Past-max-driven clique oracle parameterized by weight
$ \mathrm{Clique\_Oracle}_t(V, \sigma, w, p):\Leftrightarrow \mathrm{Clique}(V, \sigma, p) \land ~\mathrm{Threshold}_{t, \mathcal{W}}(V, \sigma, w)
Proof of validity
Lemma: Clique oracle implies max-driven property holds
$ \forall \sigma \in \Sigma_{t, \mathcal{W}}(w). ~\mathrm{Max\_Driven}(p, w) \land \mathrm{Clique\_Oracle}_t(V, \sigma, w, p) \implies \forall c \in \mathcal{E}(\sigma). ~p(c)
Lemma 1:$ \mathrm{Max\_Driven}(p, w) \land \mathrm{Max}_\mathcal{W}(\sigma, p) \implies \forall c \in \mathcal{E}(\sigma). ~p(c)
This is obvious by the definitions.
Lemma 2: $ \mathrm{Clique\_Oracle}_t(V, \sigma, w, p) \implies \mathrm{Max}(\sigma, w, p)
This is proved by lemma 3 and 4 here.
Lemma 3: $ \mathrm{Clique\_Oracle}_t(V, \sigma, w, p) \implies \mathrm{Threshold}_{t, \mathcal{W}}(\mathrm{Agreeing}(p, \sigma), w)
This is proved similarly to Lemma 37 of the original paper.
Lemma 4:$ \mathrm{Threshold}_{t, \mathcal{W}}(\mathrm{Agreeing}(p, \sigma), w) \implies \mathrm{Max}(\sigma, w, p)
Proof
$ W(\mathrm{Agreeing}(p, \sigma), w) > W(\mathcal{V}, w)/2 + t/2 - F_p(\sigma, w)
$ \iff W(\mathrm{Agreeing}(p, \sigma), w) > \{W(\mathcal{V}, w) - F_p(\sigma, w)\}/2 + \{t - F_p(\sigma, w)\}/2
$ \implies W(\mathrm{Agreeing}(p, \sigma), w) > \{W(\mathcal{V}, w) - F_p(\sigma, w)\}/2
$ \iff W(\mathrm{Agreeing}(p, \sigma), w)/2 > \{W(\mathcal{V}, w) -W(\mathrm{Agreeing}(p, \sigma), w) - F_p(\sigma, w)\}/2
$ \iff W(\mathrm{Agreeing}(p, \sigma), w) > W(\mathcal{V} \setminus \mathrm{Agreeing}(p, \sigma) \setminus E(\sigma), w)
$ \iff W(\mathrm{Agreeing}(p, \sigma), w) > W(\mathrm{Disagreeing}(p, \sigma), w)
$ \iff \mathrm{Max}(\sigma, w, p)
Lemma: Clique oracle exists in any future state where there are$ tequivocations or less by the past weight
$ \forall \sigma \in \Sigma_{t, \mathcal{W}}(w). ~\mathrm{Clique\_Oracle}_t(V, \sigma, w, p) \implies \forall \sigma' \in \mathrm{Futures}_{t, \mathcal{W}}(\sigma, w). ~\mathrm{Clique\_Oracle}_t(V, \sigma', w, p)
This is proved similarly to Lemma 39 (Cliques exist in all futures) of the original paper.
Casper TFG with validator rotation
To instantiate a blockchain consensus protocol (Casper TFG), we limit the consensus values parameter$ \mathcal{C}to a set of all possible blocks.
Modified LMD GHOST
We replace the score function used in LMD GHOST ($ \mathrm{GHOST}) to calculate a score of a block with the weight in its parent block.
$ \mathrm{Score}(b, \sigma) := \sum_{v \in \mathcal{V} : ~\exists b' \in L^H_E(\sigma)(v). ~b \downharpoonright b'} \mathrm{Weight}(\mathrm{Prev}(b))(v)
Moreover, we limit the estimator parameter$ \mathcal{E} to use LMD GHOST.
$ \mathcal{E}(\sigma) = \mathrm{GHOST}(\{g\}, \sigma) \cup \bigcup_{b \in \mathrm{GHOST}(\{g\}, \sigma)} \mathrm{Children}(b,\sigma)
Decisions in TFG
In blockchain consensus protocols, validators decide on block membership property:
$ \mathrm{P_{block}}(b) :\Leftrightarrow \lambda b'. ~b \downharpoonright b'
We introduce best children property.
$ \mathrm{P}_\mathrm{best}(b)(\sigma) :\Leftrightarrow \mathrm{P_{block}}(!\mathrm{Best\_Children}(b, \sigma))
This function check whether the input$ b'is the descendant of the best children of$ b
This enforce the tie-breaking situation i.e.$ bhas only one best child.
nrryuya.icon > This is state property so I need to fix the definition of clique, agreeing, max, etc.
Lemma: Best children property is max driven in LMD GHOST.
$ \forall b \in C. ~\forall \sigma \in \Sigma. ~\mathrm{Max\_Driven}(\mathrm{P_{best}}(b)(\sigma), \mathrm{Weight}(b))
Decision on chain.
$ \mathrm{Chain\_Decided}(bc, \sigma) :\Leftrightarrow \forall b \in bc. ~\exists V \subseteq \mathcal{V}. ~\mathrm{Clique\_Oracle}_t(V, \sigma, \mathrm{Weight}(b), \mathrm{P}_\mathrm{best}(b)(\sigma))
Blockchain safety
$ \forall bc_1, bc_2 \subseteq C. ~\forall \sigma_1, \sigma_2 \in \Sigma. ~\mathrm{Chain\_Decided}(bc_1, \sigma_1) \land \mathrm{Chain\_Decided}(bc_2, \sigma_2)
$ \implies \forall b \in bc_1 \cup bc_2. ~F(\sigma_1 \cup \sigma_2, \mathrm{Weight}(b)) \leq t
$ \implies \neg~\mathrm{Conflict}(bc_1, bc_2)
Exit rule
For liveness, "validator rotation rule" (and hence the weight estimator) must be defined so that protocol following validators can form a clique larger than the threshold.
We fix the total weight$ W_\mathrm{total}.
For simplicity, we use integers for weights.
Rate limit of exiting validators
If we allow$ \alpha("out") exit by weight for a certaion block$ b,
For clique threshold,
$ W(V) > W_\mathrm{total}/2 + t/2 - F(\sigma)
and such clique whose weight is $ W(V)must be able to form,
$ W(V) \leq W_\mathrm{total} - t - \alpha W_\mathrm{total} - F(\sigma)
The RHS is the case when all exited weights are from non-attackers and all attackers go offline
From these,$ t < (1 - 2\alpha)W_\mathrm{total}/3
Under this fault tolerance, the block can be finalized
On-chain finality
Then, for which block should we limit the exit?
For this, we introduce on-chain finality.
On-chain finality threshold (maximum fault tolernce which does not break plausible liveness.)
$ W_\mathrm{total}/2 + \{(1 - 2\alpha)W_\mathrm{total}/3\}/2 - 1 = (2 - \alpha)W_\mathrm{total}/3 - 1
For a given chain, exit transactions are valid if and only if the net weight of exitting for the oldest non-on-chain-finalized block does not excess $ \alpha.
From this, all the newer non-on-chain finalized blocks also have plausible liveness.
Q. Is there a case when a block is finalized but the parent is not finalized (under the same$ t)?
A. Yes. Practical decision making rule would be "the block is finalized and the parent is finalized".
Q. On-chain finality break "subjective finality" philosophy?
A. Maybe no (but we need further research). Validators can still do subjective decisions. Also, after on-chain finality, a block can gain more safety.
Other issues
Real liveness
Does the modification of GHOST affect the convergence of the chain?
Can we allow non-exiting decrease of weight (partial withdrawal) without any upper bound?
Catastrophe
Large equivocation faults catastrophe (safety failure)
Redo decisions by putting$ thigher
Large permanently offline faults catastrophe (liveness failure)
Instead of "inactivity leak", validators can coordinate and extend previous blocks where the weight of live validators are sufficient, ignoreing the fork choice.
(Is this the same in FFG?)
How to remove on-chain finality?